Research Group
Jacobs
Rigorous Analysis and Design (RAD)
The Rigorous Analysis and Design (RAD) group develops fundamental techniques for the analysis and design of systems with provable correctness guarantees. This includes approaches for the analysis of software with respect to safety properties and potential information leaks, as well as the automatic design of provably correct systems from formal specifications, i.e., program synthesis. One of our main research questions is how to automate the analysis and design of systems with a parametric number of components, in order to obtain correctness guarantees regardless of their size.
